home *** CD-ROM | disk | FTP | other *** search
/ Danny Amor's Online Library / Danny Amor's Online Library - Volume 1.iso / html / rfc / rfcxxx / rfc964 < prev    next >
Text File  |  1995-07-25  |  21KB  |  571 lines
  1.  
  2.  
  3. Network Working Group                                 Deepinder P. Sidhu
  4. Request for Comments: 964                               Thomas P. Blumer
  5.                                                SDC - A Burroughs Company
  6.                                                            November 1985
  7.  
  8.               SOME PROBLEMS WITH THE SPECIFICATION OF THE
  9.             MILITARY STANDARD TRANSMISSION CONTROL PROTOCOL
  10.  
  11.  
  12. STATUS OF THIS MEMO
  13.  
  14.    The purpose of this RFC is to provide helpful information on the
  15.    Military Standard Transmission Control Protocol (MIL-STD-1778) so
  16.    that one can obtain a reliable implementation of this protocol
  17.    standard. Distribution of this note is unlimited.
  18.  
  19.       Reprinted from: Proc. Protocol Specification, Testing and
  20.       Verification IV, (ed.) Y. Yemini, et al, North-Holland (1984).
  21.  
  22. ABSTRACT
  23.  
  24.    This note points out three errors with the specification of the
  25.    Military Standard Transmission Control Protocol (MIL-STD-1778, dated
  26.    August 1983 [MILS83]).  These results are based on an initial
  27.    investigation of this protocol standard.  The first problem is that
  28.    data accompanying a SYN can not be accepted because of errors in the
  29.    acceptance policy.  The second problem is that no retransmission
  30.    timer is set for a SYN packet, and therefore the SYN will not be
  31.    retransmitted if it is lost.  The third problem is that when the
  32.    connection has been established, neither entity takes the proper
  33.    steps to accept incoming data.  This note also proposes solutions to
  34.    these problems.
  35.  
  36. 1.  Introduction
  37.  
  38.    In recent years, much progress has been made in creating an
  39.    integrated set of tools for developing reliable communication
  40.    protocols.  These tools provide assistance in the specification,
  41.    verification, implementation and testing of protocols.  Several
  42.    protocols have been analyzed and developed using such tools.
  43.  
  44.    In a recent paper, the authors discussed the verification of the
  45.    connection management of NBS class 4 transport protocol (TP4).  The
  46.    verification was carried out with the help of a software tool we
  47.    developed [BLUT82] [BLUT83] [SIDD83].  In spite of the very precise
  48.    specification of this protocol, our analysis discovered several
  49.    errors in the current specification of NBS TP4.  These errors are
  50.    incompleteness errors in the specification, that is, states where
  51.    there is no transition for the reception of some input event.  Our
  52.    analysis did not find deadlocks, livelocks or any other problem in
  53.    the connection management of TP4.  In that paper, we proposed
  54.  
  55.  
  56. Sidhu & Blumer                                                  [Page 1]
  57.  
  58.  
  59.  
  60. RFC 964                                                    November 1985
  61. Some Problems with MIL-STD TCP
  62.  
  63.  
  64.    solutions for all errors except for errors associated with 2 states
  65.    whose satisfactory resolution may require redesigning parts of TP4.
  66.    Modifications to TP4 specification are currently underway to solve
  67.    the remaining incompleteness problems with 2 states.  It is important
  68.    to emphasize that we did not find any obvious error in the NBS
  69.    specification of TP4.
  70.  
  71.    The authors are currently working on the verification of connection
  72.    management of the Military Standard Transmission Control Protocol
  73.    (TCP).  This analysis will be based on the published specification
  74.    [MILS83] of TCP dated 12 August 1983.
  75.  
  76.    While studying the MIL standard TCP specification in preparation for
  77.    our analysis of the connection management features, we have noticed
  78.    several errors in the specification.  As a consequence of these
  79.    errors, the Transmission Control Protocol (as specified in [MILS83])
  80.    will not permit data to be received by TCP entities in SYN_RECVD and
  81.    ESTAB states.
  82.  
  83.    The proof of this statement follows from the specification of the
  84.    three-way handshake mechanism of TCP [MILS83] and from a decision
  85.    table associated with ESTAB state.
  86.  
  87. 2.  Transmission Control Protocol
  88.  
  89.    The Transmission Control Protocol (TCP) is a transport level
  90.    connection-oriented protocol in the DoD protocol hierarchy for use in
  91.    packet-switched and other networks.  Its most important services are
  92.    reliable transfer and ordered delivery of data over full-duplex and
  93.    flow-controlled virtual connections.  TCP is designed to operate
  94.    successfully over channels that are inherently unreliable, i.e., they
  95.    can lose, damage, duplicate, and reorder packets.
  96.  
  97.    TCP is based, in part, on a protocol discussed by Cerf and Kahn
  98.    [CERV74].  Over the years, DARPA has supported specifications of
  99.    several versions of this protocol, the last one appeared in [POSJ81].
  100.    Some issues in the connection management of this protocol are
  101.    discussed in [SUNC78].
  102.  
  103.    A few years ago, DCA decided to standardize TCP for use in DoD
  104.    networks and supported formal specification of this protocol
  105.    following the design of this protocol discussed in [POSJ81]. A
  106.    detailed specification of this protocol given in [MILS83] has been
  107.    adopted as the DoD standard for the Transmission Control Protocol, a
  108.    reliable connection-oriented transport protocol for DoD networks.
  109.  
  110.    A TCP connection progresses through three phases: opening (or
  111.  
  112.  
  113. Sidhu & Blumer                                                  [Page 2]
  114.  
  115.  
  116.  
  117. RFC 964                                                    November 1985
  118. Some Problems with MIL-STD TCP
  119.  
  120.  
  121.    synchronization), maintenance, and closing.  In this note we consider
  122.    data transfer in the opening and maintenance phases of the
  123.    connection.
  124.  
  125. 3.  Problems with MIL Standard TCP
  126.  
  127.    One basic feature of TCP is the three-way handshake which is used to
  128.    set up a properly synchronized connection between two remote TCP
  129.    entities.  This mechanism is incorrectly specified in the current
  130.    specification of TCP.  One problem is that data associated with the
  131.    SYN packet can not be delivered.  This results from an incorrect
  132.    specification of the interaction between the accept_policy action
  133.    procedure and the record_syn action procedure.  Neither of the 2
  134.    possible strategies suggested in accept_policy will give the correct
  135.    result when called from the record_syn procedure, because the
  136.    recv_next variable is updated in record_syn before the accept_policy
  137.    procedure is called.
  138.  
  139.    Another problem with the specification of the three-way handshake is
  140.    apparent in the actions listed for the Active Open event (with or
  141.    without data) when in the CLOSED state.  No retransmission timer is
  142.    set in these actions, and therefore if the initial SYN is lost, there
  143.    will be no timer expiration to trigger retransmission.  This will
  144.    prevent connection establishment if the initial SYN packet is lost by
  145.    the network.
  146.  
  147.    The third problem with the specification is that the actions for
  148.    receiving data in the ESTAB state are incorrect.  The accept action
  149.    procedure must be called when data is received, so that arriving data
  150.    may be queued and possibly passed to the user.
  151.  
  152.    A general problem with this specification is that the program
  153.    language and action table portions of the specification were clearly
  154.    not checked by any automatic syntax checking process.  Several
  155.    variable and procedure names are misspelled, and the syntax of the
  156.    action statements is often incorrect.  This can be confusing,
  157.    especially when a procedure name cannot be found in the alphabetized
  158.    list of procedures because of misspelling.
  159.  
  160.    These are some of the very serious errors that we have discovered
  161.    with the MIL standard TCP.
  162.  
  163.  
  164.  
  165.  
  166.  
  167.  
  168.  
  169.  
  170. Sidhu & Blumer                                                  [Page 3]
  171.  
  172.  
  173.  
  174. RFC 964                                                    November 1985
  175. Some Problems with MIL-STD TCP
  176.  
  177.  
  178. 4.  Detailed Discussion of the Problem
  179.  
  180.    Problem 1:  Problem with Receiving Data Accompanying SYN
  181.  
  182.       The following scenario traces the actions of 2 communicating
  183.       entities during the establishment of a connection.  Only the
  184.       simplest case is considered, i.e., the case where the connection
  185.       is established by the exchange of 3 segments.
  186.  
  187.       TCP entity A                                          TCP entity B
  188.       ------------                                          ------------
  189.  
  190.       state                segment         segment          state
  191.       transition           recvd or sent   recvd or sent    transition
  192.                            by A            by B
  193.  
  194.                                                         CLOSED -> LISTEN
  195.  
  196.       CLOSED -> SYN_SENT   SYN -->
  197.  
  198.                                            SYN -->   LISTEN -> SYN_RECVD
  199.                                            <-- SYN ACK
  200.  
  201.       SYN_SENT -> ESTAB    <-- SYN ACK
  202.                            ACK -->
  203.  
  204.                                            ACK -->    SYN_RECVD -> ESTAB
  205.  
  206.       As shown in the above diagram, 5 state transitions occur and 3 TCP
  207.       segments are exchanged during the simplest case of the three-way
  208.       handshake.  We now examine in detail the actions of each entity
  209.       during this exchange.  Special attention is given to the sequence
  210.       numbers carried in each packet and recorded in the state variables
  211.       of each entity.
  212.  
  213.       In the diagram below, the actions occurring within a procedure are
  214.       shown indented from the procedure call.  The resulting values of
  215.       sequence number variables are shown in square brackets to the
  216.       right of each statement.  The sequence number variables are shown
  217.       with the entity name (A or B) as prefix so that the two sets of
  218.       state variables may be easily distinguished.
  219.  
  220.  
  221.  
  222.  
  223.  
  224.  
  225.  
  226.  
  227. Sidhu & Blumer                                                  [Page 4]
  228.  
  229.  
  230.  
  231. RFC 964                                                    November 1985
  232. Some Problems with MIL-STD TCP
  233.  
  234.  
  235.       Transition 1 (entity B goes from state CLOSED to state LISTEN).
  236.       The user associated with entity B issues a Passive Open.
  237.  
  238.          Actions: (see p. 104)
  239.             open; (see p. 144)
  240.             new state := LISTEN;
  241.  
  242.       Transition 2 (entity A goes from state CLOSED to SYN_SENT). The
  243.       user associated with entity A issues an Active Open with Data.
  244.  
  245.          Actions: (see p. 104)
  246.             open; (see p. 144)
  247.             gen_syn(WITH_DATA); (see p. 141)
  248.                send_isn := gen_isn();                 [A.send_isn = 100]
  249.                send_next := send_isn + 1;            [A.send_next = 101]
  250.                send_una := send_isn;                  [A.send_una = 100]
  251.                seg.seq_num := send_isn;              [seg.seq_num = 100]
  252.                seg.ack_flag := FALSE;             [seg.ack_flag = FALSE]
  253.                seg.wndw := 0;                             [seg.wndw = 0]
  254.                amount := send_policy()               [assume amount > 0]
  255.             new state := SYN_SENT;
  256.  
  257.  
  258.  
  259.  
  260.  
  261.  
  262.  
  263.  
  264.  
  265.  
  266.  
  267.  
  268.  
  269.  
  270.  
  271.  
  272.  
  273.  
  274.  
  275.  
  276.  
  277.  
  278.  
  279.  
  280.  
  281.  
  282.  
  283.  
  284. Sidhu & Blumer                                                  [Page 5]
  285.  
  286.  
  287.  
  288. RFC 964                                                    November 1985
  289. Some Problems with MIL-STD TCP
  290.  
  291.  
  292.       Transition 3 (Entity B goes from state LISTEN to state SYN_RECVD).
  293.       Entity B receives the SYN segment accompanying data sent by entity
  294.       A.
  295.  
  296.          Actions: (see p. 106)
  297.             (since this segment has no RESET, no ACK, does have SYN, and
  298.             we assume reasonable security and precedence parameters, row
  299.             3 of the table applies)
  300.             record_syn; (see p. 147)
  301.                recv_isn := seg.seq_num; [B.recv_isn = seg_seq_num = 100]
  302.                recv_next := recv_isn + 1;            [B.recv_next = 101]
  303.                if seg.ack_flag then
  304.                   send_una := seg.ack_num;                   [no change]
  305.                accept_policy; (see p. 131)
  306.                   Accept in-order data only:
  307.                      Acceptance Test is
  308.                         seg.seq_num = recv_next;
  309.                   Accept any data within the receive window:
  310.                      Acceptance Test has two parts
  311.                         recv_next =< seg.seq_num =< recv_next +
  312.                                                                recv_wndw
  313.                         or
  314.                         recv_next =< seg.seq_num + length =<
  315.                                                    recv_next + recv_wndw
  316.                         ********************************************
  317.                            An error occurs here, with either possible
  318.                            strategy given in accept_policy, because
  319.                            recv_next > seg.seq_num.  Therefore
  320.                            accept_policy will incorrectly indicate that
  321.                            the data cannot be accepted.
  322.                         ********************************************
  323.             gen_syn(WITH_ACK); (see p. 141)
  324.                send_isn := gen_isn();                 [B.send_isn = 300]
  325.                send_next := send_isn + 1;            [B.send_next = 301]
  326.                send_una := send_isn;                  [B.send_una = 300]
  327.                seg.seq_num := send_next;             [seg.seq_num = 301]
  328.                seg.ack_flag := TRUE;               [seg.ack_flag = TRUE]
  329.                seg.ack_num := recv_isn + 1;          [seg.ack_num = 102]
  330.             new state := SYN_RECVD;
  331.  
  332.  
  333.  
  334.  
  335.  
  336.  
  337.  
  338.  
  339.  
  340.  
  341. Sidhu & Blumer                                                  [Page 6]
  342.  
  343.  
  344.  
  345. RFC 964                                                    November 1985
  346. Some Problems with MIL-STD TCP
  347.  
  348.  
  349.       Transition 4 (entity A goes from state SYN_SENT to ESTAB) Entity A
  350.       receives the SYN ACK sent by entity B.
  351.  
  352.          Actions: (see p. 107)
  353.             In order to select the applicable row of the table on p.
  354.             107, we first evaluate the decision function
  355.             ACK_status_test1.
  356.                ACK_status_test1();
  357.                   if(seg.ack_flag = FALSE) then
  358.                      return(NONE);
  359.                   if(seg.ack_num <= send_una) or
  360.                      (seg.ack_num > send_next) then
  361.                         return(INVALID)
  362.                   else
  363.                      return(VALID);
  364.  
  365.                   ... and so on.
  366.  
  367.       The important thing to notice in the above scenario is the error
  368.       that occurs in transition 3, where the wrong value for recv_next
  369.       leads to the routine record_syn refusing to accept the data.
  370.  
  371.    Problem 2:  Problem with Retransmission of SYN Packet
  372.  
  373.       The actions listed for Active Open (with or without data; see p.
  374.       103) are calls to the routines open and gen_syn.  Neither of these
  375.       routines (or routines that they call) explicitly sets a
  376.       retransmission timer.  Therefore if the initial SYN is lost there
  377.       is no timer expiration to trigger retransmission of the SYN.  If
  378.       this happens, the TCP will fail in its attempt to establish the
  379.       desired connection with a remote TCP.
  380.  
  381.       Note that this differs with the actions specified for transmission
  382.       of data from the ESTAB state.  In that transition the routine
  383.       dispatch (p. 137) is called first which in turn calls the routine
  384.       send_new_data (p.  156).  One of actions of the last routine is to
  385.       start a retransmission timer for the newly sent data.
  386.  
  387.  
  388.  
  389.  
  390.  
  391.  
  392.  
  393.  
  394.  
  395.  
  396.  
  397.  
  398. Sidhu & Blumer                                                  [Page 7]
  399.  
  400.  
  401.  
  402. RFC 964                                                    November 1985
  403. Some Problems with MIL-STD TCP
  404.  
  405.  
  406.    Problem 3:  Problem with Receiving Data in TCP ESTAB State
  407.  
  408.       When both entities are in the state ESTAB, and one sends data to
  409.       the other, an error in the actions of the receiver prohibits the
  410.       data from being accepted.  The following simple scenario
  411.       illustrates the problem.  Here the user associated with entity A
  412.       issues a Send request, and A sends data to entity B.  When B
  413.       receives the data it replies with an acknowledgment.
  414.  
  415.       TCP entity A                                          TCP entity B
  416.       ------------                                          ------------
  417.  
  418.       state                segment         segment          state
  419.       transition           recvd or sent   recvd or sent    transition
  420.                            by A            by B
  421.  
  422.       ESTAB -> ESTAB       DATA -->
  423.  
  424.                                            DATA -->       ESTAB -> ESTAB
  425.                                            <-- ACK
  426.  
  427.       Transition 1 (entity A goes from state ESTAB to ESTAB) Entity A
  428.       sends data packet to entity B.
  429.  
  430.          Actions: (see p. 110)
  431.             dispatch; (see p. 137)
  432.  
  433.       Transition 2 (entity B goes from state ESTAB to ESTAB) Entity B
  434.       receives data packet from entity B.
  435.  
  436.          Actions: (see p. 111)
  437.             Assuming the data is in order and valid, we use row 6 of the
  438.             table.
  439.             update; (see p. 159)
  440.             ************************************************************
  441.                An error occurs here, because the routine update does
  442.                nothing to accept the incoming data, or to arrange to
  443.                pass it on to the user.
  444.             ************************************************************
  445.  
  446.  
  447.  
  448.  
  449.  
  450.  
  451.  
  452.  
  453.  
  454.  
  455. Sidhu & Blumer                                                  [Page 8]
  456.  
  457.  
  458.  
  459. RFC 964                                                    November 1985
  460. Some Problems with MIL-STD TCP
  461.  
  462.  
  463. 5.  Solutions to Problems
  464.  
  465.    The problem with record_syn and accept_policy can be solved by having
  466.    record_syn call accept_policy before the variable recv_next is
  467.    updated.
  468.  
  469.    The problem with gen_syn can be corrected by having gen_syn or open
  470.    explicitly request the retransmission timer.
  471.  
  472.    The problem with the reception of data in the ESTAB state is
  473.    apparently caused by the transposition of the action tables on pages
  474.    111 and 112.  These tables should be interchanged.  This solution
  475.    will also correct a related problem, namely that an entity can never
  476.    reach the CLOSE_WAIT state from the ESTAB state.
  477.  
  478.    Syntax errors in the action statements and tables could be easily
  479.    caught by an automatic syntax checker if the document used a more
  480.    formal description technique.  This would be difficult to do for
  481.    [MILS83] since this document is not based on a formalized description
  482.    technique [BREM83].
  483.  
  484.    The errors pointed out in this note have been submitted to DCA and
  485.    will be corrected in the next update of the MIL STD TCP
  486.    specification.
  487.  
  488. 6.  Implementation of MIL Standard TCP
  489.  
  490.    In the discussion above, we pointed out several serious errors in the
  491.    specification of the Military Standard Transmission Control Protocol
  492.    [MILS83].  These errors imply that a TCP implementation that
  493.    faithfully conforms to the Military TCP standard will not be able to
  494.  
  495.       Receive data sent with a SYN packet.
  496.  
  497.       Establish a connection if the initial SYN packet is lost.
  498.  
  499.       Receive data when in the ESTAB state.
  500.  
  501.    It also follows from our discussion that an implementation of MIL
  502.    Standard TCP [MILS83] must include corrections mentioned above to get
  503.    a running TCP.
  504.  
  505.    The problems pointed out in this paper with the current specification
  506.    of the MIL Standard TCP [MILS83] are based on an initial
  507.    investigation of this protocol standard by the authors.
  508.  
  509.  
  510.  
  511.  
  512. Sidhu & Blumer                                                  [Page 9]
  513.  
  514.  
  515.  
  516. RFC 964                                                    November 1985
  517. Some Problems with MIL-STD TCP
  518.  
  519.  
  520. REFERENCES
  521.  
  522.    [BLUT83]  Blumer, T. P., and Sidhu, D. P., "Mechanical Verification
  523.              and Automatic Implementation of Authentication Protocols
  524.              for Computer Networks", SDC Burroughs Report (1983),
  525.              submitted for publication.
  526.  
  527.    [BLUT82]  Blumer, T. P., and Tenney, R. L., "A Formal Specification
  528.              Technique and Implementation Method for Protocols",
  529.              Computer Networks, Vol. 6, No. 3, July 1982, pp. 201-217.
  530.  
  531.    [BREM83]  Breslin, M., Pollack, R. and Sidhu D. P., "Formalization of
  532.              DoD Protocol Specification Technique", SDC - Burroughs
  533.              Report 1983.
  534.  
  535.    [CERV74]  Cerf, V., and Kahn, R., "A Protocol for Packet Network
  536.              Interconnection", IEEE Trans. Comm., May 1974.
  537.  
  538.    [MILS83]  "Military Standard Transmission Control Protocol",
  539.              MIL-STD-1778, 12 August 1983.
  540.  
  541.    [POSJ81]  Postel, J. (ed.), "DoD Standard Transmission Control
  542.              Protocol", Defense Advanced Research Projects Agency,
  543.              Information Processing Techniques Office, RFC-793,
  544.              September 1981.
  545.  
  546.    [SIDD83]  Sidhu, D. P., and Blumer, T. P., "Verification of NBS Class
  547.              4 Transport Protocol", SDC Burroughs Report (1983),
  548.              submitted for publication.
  549.  
  550.    [SUNC78]  Sunshine, C., and Dalal, Y., "Connection Management in
  551.              Transport Protocols", Computer Networks, Vol. 2, pp.454-473
  552.              (1978).
  553.  
  554.  
  555.  
  556.  
  557.  
  558.  
  559.  
  560.  
  561.  
  562.  
  563.  
  564.  
  565.  
  566.  
  567.  
  568.  
  569. Sidhu & Blumer                                                 [Page 10]
  570.  
  571.